\begin{tabbing}
$\forall$$A$, $B$:Realizer.
\\[0ex]R{-}Feasible($A$)
\\[0ex]$\Rightarrow$ R{-}Feasible($B$)
\\[0ex]$\Rightarrow$ $A$ $\parallel$ $B$
\\[0ex]$\Rightarrow$ (\=$\forall$$k$:Knd.\+
\\[0ex]isrcv($k$) $\Rightarrow$ R{-}da($A$;source(lnk($k$)))($k$)?Void $\subseteq\rho$ Valtype(R{-}da($B$;destination(lnk($k$)));$k$))
\-
\end{tabbing}